H-Termination proof of /home/matraf/haskell/eval_FullyBlown

MAYBE 40.249 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ BR

mainModule Main

((range :: (Int,Int) -> [Int]) :: (Int,Int) -> [Int])

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((range :: (Int,Int) -> [Int]) :: (Int,Int) -> [Int])

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

takeWhile p [] = []

takeWhile p (x : xs)

| p x

= x : takeWhile p xs

| otherwise

= []

is transformed to

takeWhile p [] = takeWhile3 p []

takeWhile p (x : xs) = takeWhile2 p (x : xs)

takeWhile1 p x xs True = x : takeWhile p xs

takeWhile1 p x xs False = takeWhile0 p x xs otherwise

takeWhile0 p x xs True = []

takeWhile2 p (x : xs) = takeWhile1 p x xs (p x)

takeWhile3 p [] = []

takeWhile3 vz wu = takeWhile2 vz wu

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((range :: (Int,Int) -> [Int]) :: (Int,Int) -> [Int])

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

mainModule Main

(range :: (Int,Int) -> [Int])

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="range",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="range wv3",fontsize=16,color="burlywood",shape="triangle"];949[label="wv3/(wv30,wv31)",fontsize=10,color="white",style="solid",shape="box"];3 -> 949[label="",style="solid", color="burlywood", weight=9];
949 -> 4[label="",style="solid", color="burlywood", weight=3];
4[label="range (wv30,wv31)",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="enumFromTo wv30 wv31",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="numericEnumFromTo wv30 wv31",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="takeWhile (flip (<=) wv31) (numericEnumFrom wv30)",fontsize=16,color="black",shape="triangle"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="takeWhile (flip (<=) wv31) (wv30 : (numericEnumFrom $! wv30 + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="takeWhile2 (flip (<=) wv31) (wv30 : (numericEnumFrom $! wv30 + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="takeWhile1 (flip (<=) wv31) wv30 (numericEnumFrom $! wv30 + fromInt (Pos (Succ Zero))) (flip (<=) wv31 wv30)",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="takeWhile1 (flip (<=) wv31) wv30 (numericEnumFrom $! wv30 + fromInt (Pos (Succ Zero))) ((<=) wv30 wv31)",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="takeWhile1 (flip (<=) wv31) wv30 (numericEnumFrom $! wv30 + fromInt (Pos (Succ Zero))) (compare wv30 wv31 /= GT)",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="takeWhile1 (flip (<=) wv31) wv30 (numericEnumFrom $! wv30 + fromInt (Pos (Succ Zero))) (not (compare wv30 wv31 == GT))",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="takeWhile1 (flip (<=) wv31) wv30 (numericEnumFrom $! wv30 + fromInt (Pos (Succ Zero))) (not (primCmpInt wv30 wv31 == GT))",fontsize=16,color="burlywood",shape="box"];950[label="wv30/Pos wv300",fontsize=10,color="white",style="solid",shape="box"];14 -> 950[label="",style="solid", color="burlywood", weight=9];
950 -> 15[label="",style="solid", color="burlywood", weight=3];
951[label="wv30/Neg wv300",fontsize=10,color="white",style="solid",shape="box"];14 -> 951[label="",style="solid", color="burlywood", weight=9];
951 -> 16[label="",style="solid", color="burlywood", weight=3];
15[label="takeWhile1 (flip (<=) wv31) (Pos wv300) (numericEnumFrom $! Pos wv300 + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos wv300) wv31 == GT))",fontsize=16,color="burlywood",shape="box"];952[label="wv300/Succ wv3000",fontsize=10,color="white",style="solid",shape="box"];15 -> 952[label="",style="solid", color="burlywood", weight=9];
952 -> 17[label="",style="solid", color="burlywood", weight=3];
953[label="wv300/Zero",fontsize=10,color="white",style="solid",shape="box"];15 -> 953[label="",style="solid", color="burlywood", weight=9];
953 -> 18[label="",style="solid", color="burlywood", weight=3];
16[label="takeWhile1 (flip (<=) wv31) (Neg wv300) (numericEnumFrom $! Neg wv300 + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg wv300) wv31 == GT))",fontsize=16,color="burlywood",shape="box"];954[label="wv300/Succ wv3000",fontsize=10,color="white",style="solid",shape="box"];16 -> 954[label="",style="solid", color="burlywood", weight=9];
954 -> 19[label="",style="solid", color="burlywood", weight=3];
955[label="wv300/Zero",fontsize=10,color="white",style="solid",shape="box"];16 -> 955[label="",style="solid", color="burlywood", weight=9];
955 -> 20[label="",style="solid", color="burlywood", weight=3];
17[label="takeWhile1 (flip (<=) wv31) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos (Succ wv3000)) wv31 == GT))",fontsize=16,color="burlywood",shape="box"];956[label="wv31/Pos wv310",fontsize=10,color="white",style="solid",shape="box"];17 -> 956[label="",style="solid", color="burlywood", weight=9];
956 -> 21[label="",style="solid", color="burlywood", weight=3];
957[label="wv31/Neg wv310",fontsize=10,color="white",style="solid",shape="box"];17 -> 957[label="",style="solid", color="burlywood", weight=9];
957 -> 22[label="",style="solid", color="burlywood", weight=3];
18[label="takeWhile1 (flip (<=) wv31) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos Zero) wv31 == GT))",fontsize=16,color="burlywood",shape="box"];958[label="wv31/Pos wv310",fontsize=10,color="white",style="solid",shape="box"];18 -> 958[label="",style="solid", color="burlywood", weight=9];
958 -> 23[label="",style="solid", color="burlywood", weight=3];
959[label="wv31/Neg wv310",fontsize=10,color="white",style="solid",shape="box"];18 -> 959[label="",style="solid", color="burlywood", weight=9];
959 -> 24[label="",style="solid", color="burlywood", weight=3];
19[label="takeWhile1 (flip (<=) wv31) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg (Succ wv3000)) wv31 == GT))",fontsize=16,color="burlywood",shape="box"];960[label="wv31/Pos wv310",fontsize=10,color="white",style="solid",shape="box"];19 -> 960[label="",style="solid", color="burlywood", weight=9];
960 -> 25[label="",style="solid", color="burlywood", weight=3];
961[label="wv31/Neg wv310",fontsize=10,color="white",style="solid",shape="box"];19 -> 961[label="",style="solid", color="burlywood", weight=9];
961 -> 26[label="",style="solid", color="burlywood", weight=3];
20[label="takeWhile1 (flip (<=) wv31) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg Zero) wv31 == GT))",fontsize=16,color="burlywood",shape="box"];962[label="wv31/Pos wv310",fontsize=10,color="white",style="solid",shape="box"];20 -> 962[label="",style="solid", color="burlywood", weight=9];
962 -> 27[label="",style="solid", color="burlywood", weight=3];
963[label="wv31/Neg wv310",fontsize=10,color="white",style="solid",shape="box"];20 -> 963[label="",style="solid", color="burlywood", weight=9];
963 -> 28[label="",style="solid", color="burlywood", weight=3];
21[label="takeWhile1 (flip (<=) (Pos wv310)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos (Succ wv3000)) (Pos wv310) == GT))",fontsize=16,color="black",shape="box"];21 -> 29[label="",style="solid", color="black", weight=3];
22[label="takeWhile1 (flip (<=) (Neg wv310)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos (Succ wv3000)) (Neg wv310) == GT))",fontsize=16,color="black",shape="box"];22 -> 30[label="",style="solid", color="black", weight=3];
23[label="takeWhile1 (flip (<=) (Pos wv310)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos Zero) (Pos wv310) == GT))",fontsize=16,color="burlywood",shape="box"];964[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];23 -> 964[label="",style="solid", color="burlywood", weight=9];
964 -> 31[label="",style="solid", color="burlywood", weight=3];
965[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];23 -> 965[label="",style="solid", color="burlywood", weight=9];
965 -> 32[label="",style="solid", color="burlywood", weight=3];
24[label="takeWhile1 (flip (<=) (Neg wv310)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos Zero) (Neg wv310) == GT))",fontsize=16,color="burlywood",shape="box"];966[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];24 -> 966[label="",style="solid", color="burlywood", weight=9];
966 -> 33[label="",style="solid", color="burlywood", weight=3];
967[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];24 -> 967[label="",style="solid", color="burlywood", weight=9];
967 -> 34[label="",style="solid", color="burlywood", weight=3];
25[label="takeWhile1 (flip (<=) (Pos wv310)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg (Succ wv3000)) (Pos wv310) == GT))",fontsize=16,color="black",shape="box"];25 -> 35[label="",style="solid", color="black", weight=3];
26[label="takeWhile1 (flip (<=) (Neg wv310)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg (Succ wv3000)) (Neg wv310) == GT))",fontsize=16,color="black",shape="box"];26 -> 36[label="",style="solid", color="black", weight=3];
27[label="takeWhile1 (flip (<=) (Pos wv310)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg Zero) (Pos wv310) == GT))",fontsize=16,color="burlywood",shape="box"];968[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];27 -> 968[label="",style="solid", color="burlywood", weight=9];
968 -> 37[label="",style="solid", color="burlywood", weight=3];
969[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];27 -> 969[label="",style="solid", color="burlywood", weight=9];
969 -> 38[label="",style="solid", color="burlywood", weight=3];
28[label="takeWhile1 (flip (<=) (Neg wv310)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg Zero) (Neg wv310) == GT))",fontsize=16,color="burlywood",shape="box"];970[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];28 -> 970[label="",style="solid", color="burlywood", weight=9];
970 -> 39[label="",style="solid", color="burlywood", weight=3];
971[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];28 -> 971[label="",style="solid", color="burlywood", weight=9];
971 -> 40[label="",style="solid", color="burlywood", weight=3];
29[label="takeWhile1 (flip (<=) (Pos wv310)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv3000) wv310 == GT))",fontsize=16,color="burlywood",shape="box"];972[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];29 -> 972[label="",style="solid", color="burlywood", weight=9];
972 -> 41[label="",style="solid", color="burlywood", weight=3];
973[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];29 -> 973[label="",style="solid", color="burlywood", weight=9];
973 -> 42[label="",style="solid", color="burlywood", weight=3];
30[label="takeWhile1 (flip (<=) (Neg wv310)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (GT == GT))",fontsize=16,color="black",shape="box"];30 -> 43[label="",style="solid", color="black", weight=3];
31[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos Zero) (Pos (Succ wv3100)) == GT))",fontsize=16,color="black",shape="box"];31 -> 44[label="",style="solid", color="black", weight=3];
32[label="takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos Zero) (Pos Zero) == GT))",fontsize=16,color="black",shape="box"];32 -> 45[label="",style="solid", color="black", weight=3];
33[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos Zero) (Neg (Succ wv3100)) == GT))",fontsize=16,color="black",shape="box"];33 -> 46[label="",style="solid", color="black", weight=3];
34[label="takeWhile1 (flip (<=) (Neg Zero)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Pos Zero) (Neg Zero) == GT))",fontsize=16,color="black",shape="box"];34 -> 47[label="",style="solid", color="black", weight=3];
35[label="takeWhile1 (flip (<=) (Pos wv310)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (LT == GT))",fontsize=16,color="black",shape="box"];35 -> 48[label="",style="solid", color="black", weight=3];
36[label="takeWhile1 (flip (<=) (Neg wv310)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpNat wv310 (Succ wv3000) == GT))",fontsize=16,color="burlywood",shape="box"];974[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];36 -> 974[label="",style="solid", color="burlywood", weight=9];
974 -> 49[label="",style="solid", color="burlywood", weight=3];
975[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];36 -> 975[label="",style="solid", color="burlywood", weight=9];
975 -> 50[label="",style="solid", color="burlywood", weight=3];
37[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg Zero) (Pos (Succ wv3100)) == GT))",fontsize=16,color="black",shape="box"];37 -> 51[label="",style="solid", color="black", weight=3];
38[label="takeWhile1 (flip (<=) (Pos Zero)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg Zero) (Pos Zero) == GT))",fontsize=16,color="black",shape="box"];38 -> 52[label="",style="solid", color="black", weight=3];
39[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg Zero) (Neg (Succ wv3100)) == GT))",fontsize=16,color="black",shape="box"];39 -> 53[label="",style="solid", color="black", weight=3];
40[label="takeWhile1 (flip (<=) (Neg Zero)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (primCmpInt (Neg Zero) (Neg Zero) == GT))",fontsize=16,color="black",shape="box"];40 -> 54[label="",style="solid", color="black", weight=3];
41[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv3000) (Succ wv3100) == GT))",fontsize=16,color="black",shape="box"];41 -> 55[label="",style="solid", color="black", weight=3];
42[label="takeWhile1 (flip (<=) (Pos Zero)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv3000) Zero == GT))",fontsize=16,color="black",shape="box"];42 -> 56[label="",style="solid", color="black", weight=3];
43[label="takeWhile1 (flip (<=) (Neg wv310)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not True)",fontsize=16,color="black",shape="box"];43 -> 57[label="",style="solid", color="black", weight=3];
44[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (primCmpNat Zero (Succ wv3100) == GT))",fontsize=16,color="black",shape="box"];44 -> 58[label="",style="solid", color="black", weight=3];
45[label="takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (EQ == GT))",fontsize=16,color="black",shape="box"];45 -> 59[label="",style="solid", color="black", weight=3];
46[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (GT == GT))",fontsize=16,color="black",shape="box"];46 -> 60[label="",style="solid", color="black", weight=3];
47[label="takeWhile1 (flip (<=) (Neg Zero)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (EQ == GT))",fontsize=16,color="black",shape="box"];47 -> 61[label="",style="solid", color="black", weight=3];
48[label="takeWhile1 (flip (<=) (Pos wv310)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="box"];48 -> 62[label="",style="solid", color="black", weight=3];
49[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv3100) (Succ wv3000) == GT))",fontsize=16,color="black",shape="box"];49 -> 63[label="",style="solid", color="black", weight=3];
50[label="takeWhile1 (flip (<=) (Neg Zero)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpNat Zero (Succ wv3000) == GT))",fontsize=16,color="black",shape="box"];50 -> 64[label="",style="solid", color="black", weight=3];
51[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (LT == GT))",fontsize=16,color="black",shape="box"];51 -> 65[label="",style="solid", color="black", weight=3];
52[label="takeWhile1 (flip (<=) (Pos Zero)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (EQ == GT))",fontsize=16,color="black",shape="box"];52 -> 66[label="",style="solid", color="black", weight=3];
53[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv3100) Zero == GT))",fontsize=16,color="black",shape="box"];53 -> 67[label="",style="solid", color="black", weight=3];
54[label="takeWhile1 (flip (<=) (Neg Zero)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (EQ == GT))",fontsize=16,color="black",shape="box"];54 -> 68[label="",style="solid", color="black", weight=3];
55 -> 789[label="",style="dashed", color="red", weight=0];
55[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpNat wv3000 wv3100 == GT))",fontsize=16,color="magenta"];55 -> 790[label="",style="dashed", color="magenta", weight=3];
55 -> 791[label="",style="dashed", color="magenta", weight=3];
55 -> 792[label="",style="dashed", color="magenta", weight=3];
55 -> 793[label="",style="dashed", color="magenta", weight=3];
56[label="takeWhile1 (flip (<=) (Pos Zero)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (GT == GT))",fontsize=16,color="black",shape="box"];56 -> 71[label="",style="solid", color="black", weight=3];
57[label="takeWhile1 (flip (<=) (Neg wv310)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) False",fontsize=16,color="black",shape="box"];57 -> 72[label="",style="solid", color="black", weight=3];
58[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not (LT == GT))",fontsize=16,color="black",shape="box"];58 -> 73[label="",style="solid", color="black", weight=3];
59[label="takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="box"];59 -> 74[label="",style="solid", color="black", weight=3];
60[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not True)",fontsize=16,color="black",shape="box"];60 -> 75[label="",style="solid", color="black", weight=3];
61[label="takeWhile1 (flip (<=) (Neg Zero)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="box"];61 -> 76[label="",style="solid", color="black", weight=3];
62[label="takeWhile1 (flip (<=) (Pos wv310)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];62 -> 77[label="",style="solid", color="black", weight=3];
63 -> 835[label="",style="dashed", color="red", weight=0];
63[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (primCmpNat wv3100 wv3000 == GT))",fontsize=16,color="magenta"];63 -> 836[label="",style="dashed", color="magenta", weight=3];
63 -> 837[label="",style="dashed", color="magenta", weight=3];
63 -> 838[label="",style="dashed", color="magenta", weight=3];
63 -> 839[label="",style="dashed", color="magenta", weight=3];
64[label="takeWhile1 (flip (<=) (Neg Zero)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not (LT == GT))",fontsize=16,color="black",shape="box"];64 -> 80[label="",style="solid", color="black", weight=3];
65[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="box"];65 -> 81[label="",style="solid", color="black", weight=3];
66[label="takeWhile1 (flip (<=) (Pos Zero)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="box"];66 -> 82[label="",style="solid", color="black", weight=3];
67[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not (GT == GT))",fontsize=16,color="black",shape="box"];67 -> 83[label="",style="solid", color="black", weight=3];
68[label="takeWhile1 (flip (<=) (Neg Zero)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="box"];68 -> 84[label="",style="solid", color="black", weight=3];
790[label="wv3100",fontsize=16,color="green",shape="box"];791[label="wv3100",fontsize=16,color="green",shape="box"];792[label="wv3000",fontsize=16,color="green",shape="box"];793[label="wv3000",fontsize=16,color="green",shape="box"];789[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (primCmpNat wv52 wv53 == GT))",fontsize=16,color="burlywood",shape="triangle"];978[label="wv52/Succ wv520",fontsize=10,color="white",style="solid",shape="box"];789 -> 978[label="",style="solid", color="burlywood", weight=9];
978 -> 830[label="",style="solid", color="burlywood", weight=3];
979[label="wv52/Zero",fontsize=10,color="white",style="solid",shape="box"];789 -> 979[label="",style="solid", color="burlywood", weight=9];
979 -> 831[label="",style="solid", color="burlywood", weight=3];
71[label="takeWhile1 (flip (<=) (Pos Zero)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) (not True)",fontsize=16,color="black",shape="box"];71 -> 89[label="",style="solid", color="black", weight=3];
72[label="takeWhile0 (flip (<=) (Neg wv310)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) otherwise",fontsize=16,color="black",shape="box"];72 -> 90[label="",style="solid", color="black", weight=3];
73[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="box"];73 -> 91[label="",style="solid", color="black", weight=3];
74[label="takeWhile1 (flip (<=) (Pos Zero)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];74 -> 92[label="",style="solid", color="black", weight=3];
75[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) False",fontsize=16,color="black",shape="box"];75 -> 93[label="",style="solid", color="black", weight=3];
76[label="takeWhile1 (flip (<=) (Neg Zero)) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];76 -> 94[label="",style="solid", color="black", weight=3];
77[label="Neg (Succ wv3000) : takeWhile (flip (<=) (Pos wv310)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];77 -> 95[label="",style="dashed", color="green", weight=3];
836[label="wv3000",fontsize=16,color="green",shape="box"];837[label="wv3000",fontsize=16,color="green",shape="box"];838[label="wv3100",fontsize=16,color="green",shape="box"];839[label="wv3100",fontsize=16,color="green",shape="box"];835[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (primCmpNat wv57 wv58 == GT))",fontsize=16,color="burlywood",shape="triangle"];980[label="wv57/Succ wv570",fontsize=10,color="white",style="solid",shape="box"];835 -> 980[label="",style="solid", color="burlywood", weight=9];
980 -> 876[label="",style="solid", color="burlywood", weight=3];
981[label="wv57/Zero",fontsize=10,color="white",style="solid",shape="box"];835 -> 981[label="",style="solid", color="burlywood", weight=9];
981 -> 877[label="",style="solid", color="burlywood", weight=3];
80[label="takeWhile1 (flip (<=) (Neg Zero)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="box"];80 -> 100[label="",style="solid", color="black", weight=3];
81[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];81 -> 101[label="",style="solid", color="black", weight=3];
82[label="takeWhile1 (flip (<=) (Pos Zero)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];82 -> 102[label="",style="solid", color="black", weight=3];
83[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) (not True)",fontsize=16,color="black",shape="box"];83 -> 103[label="",style="solid", color="black", weight=3];
84[label="takeWhile1 (flip (<=) (Neg Zero)) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];84 -> 104[label="",style="solid", color="black", weight=3];
830[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv520) wv53 == GT))",fontsize=16,color="burlywood",shape="box"];982[label="wv53/Succ wv530",fontsize=10,color="white",style="solid",shape="box"];830 -> 982[label="",style="solid", color="burlywood", weight=9];
982 -> 878[label="",style="solid", color="burlywood", weight=3];
983[label="wv53/Zero",fontsize=10,color="white",style="solid",shape="box"];830 -> 983[label="",style="solid", color="burlywood", weight=9];
983 -> 879[label="",style="solid", color="burlywood", weight=3];
831[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (primCmpNat Zero wv53 == GT))",fontsize=16,color="burlywood",shape="box"];984[label="wv53/Succ wv530",fontsize=10,color="white",style="solid",shape="box"];831 -> 984[label="",style="solid", color="burlywood", weight=9];
984 -> 880[label="",style="solid", color="burlywood", weight=3];
985[label="wv53/Zero",fontsize=10,color="white",style="solid",shape="box"];831 -> 985[label="",style="solid", color="burlywood", weight=9];
985 -> 881[label="",style="solid", color="burlywood", weight=3];
89[label="takeWhile1 (flip (<=) (Pos Zero)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) False",fontsize=16,color="black",shape="box"];89 -> 109[label="",style="solid", color="black", weight=3];
90[label="takeWhile0 (flip (<=) (Neg wv310)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];90 -> 110[label="",style="solid", color="black", weight=3];
91[label="takeWhile1 (flip (<=) (Pos (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];91 -> 111[label="",style="solid", color="black", weight=3];
92[label="Pos Zero : takeWhile (flip (<=) (Pos Zero)) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];92 -> 112[label="",style="dashed", color="green", weight=3];
93[label="takeWhile0 (flip (<=) (Neg (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) otherwise",fontsize=16,color="black",shape="box"];93 -> 113[label="",style="solid", color="black", weight=3];
94[label="Pos Zero : takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];94 -> 114[label="",style="dashed", color="green", weight=3];
95[label="takeWhile (flip (<=) (Pos wv310)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];95 -> 115[label="",style="solid", color="black", weight=3];
876[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv570) wv58 == GT))",fontsize=16,color="burlywood",shape="box"];986[label="wv58/Succ wv580",fontsize=10,color="white",style="solid",shape="box"];876 -> 986[label="",style="solid", color="burlywood", weight=9];
986 -> 882[label="",style="solid", color="burlywood", weight=3];
987[label="wv58/Zero",fontsize=10,color="white",style="solid",shape="box"];876 -> 987[label="",style="solid", color="burlywood", weight=9];
987 -> 883[label="",style="solid", color="burlywood", weight=3];
877[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (primCmpNat Zero wv58 == GT))",fontsize=16,color="burlywood",shape="box"];988[label="wv58/Succ wv580",fontsize=10,color="white",style="solid",shape="box"];877 -> 988[label="",style="solid", color="burlywood", weight=9];
988 -> 884[label="",style="solid", color="burlywood", weight=3];
989[label="wv58/Zero",fontsize=10,color="white",style="solid",shape="box"];877 -> 989[label="",style="solid", color="burlywood", weight=9];
989 -> 885[label="",style="solid", color="burlywood", weight=3];
100[label="takeWhile1 (flip (<=) (Neg Zero)) (Neg (Succ wv3000)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];100 -> 120[label="",style="solid", color="black", weight=3];
101[label="Neg Zero : takeWhile (flip (<=) (Pos (Succ wv3100))) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];101 -> 121[label="",style="dashed", color="green", weight=3];
102[label="Neg Zero : takeWhile (flip (<=) (Pos Zero)) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];102 -> 122[label="",style="dashed", color="green", weight=3];
103[label="takeWhile1 (flip (<=) (Neg (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) False",fontsize=16,color="black",shape="box"];103 -> 123[label="",style="solid", color="black", weight=3];
104[label="Neg Zero : takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];104 -> 124[label="",style="dashed", color="green", weight=3];
878[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv520) (Succ wv530) == GT))",fontsize=16,color="black",shape="box"];878 -> 886[label="",style="solid", color="black", weight=3];
879[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv520) Zero == GT))",fontsize=16,color="black",shape="box"];879 -> 887[label="",style="solid", color="black", weight=3];
880[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (primCmpNat Zero (Succ wv530) == GT))",fontsize=16,color="black",shape="box"];880 -> 888[label="",style="solid", color="black", weight=3];
881[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];881 -> 889[label="",style="solid", color="black", weight=3];
109[label="takeWhile0 (flip (<=) (Pos Zero)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) otherwise",fontsize=16,color="black",shape="box"];109 -> 130[label="",style="solid", color="black", weight=3];
110[label="[]",fontsize=16,color="green",shape="box"];111[label="Pos Zero : takeWhile (flip (<=) (Pos (Succ wv3100))) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];111 -> 131[label="",style="dashed", color="green", weight=3];
112[label="takeWhile (flip (<=) (Pos Zero)) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];112 -> 132[label="",style="solid", color="black", weight=3];
113[label="takeWhile0 (flip (<=) (Neg (Succ wv3100))) (Pos Zero) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];113 -> 133[label="",style="solid", color="black", weight=3];
114[label="takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];114 -> 134[label="",style="solid", color="black", weight=3];
115[label="takeWhile (flip (<=) (Pos wv310)) (Neg (Succ wv3000) + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Neg (Succ wv3000) + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];115 -> 135[label="",style="solid", color="black", weight=3];
882[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv570) (Succ wv580) == GT))",fontsize=16,color="black",shape="box"];882 -> 890[label="",style="solid", color="black", weight=3];
883[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (primCmpNat (Succ wv570) Zero == GT))",fontsize=16,color="black",shape="box"];883 -> 891[label="",style="solid", color="black", weight=3];
884[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (primCmpNat Zero (Succ wv580) == GT))",fontsize=16,color="black",shape="box"];884 -> 892[label="",style="solid", color="black", weight=3];
885[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];885 -> 893[label="",style="solid", color="black", weight=3];
120[label="Neg (Succ wv3000) : takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];120 -> 141[label="",style="dashed", color="green", weight=3];
121[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];121 -> 142[label="",style="solid", color="black", weight=3];
122[label="takeWhile (flip (<=) (Pos Zero)) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];122 -> 143[label="",style="solid", color="black", weight=3];
123[label="takeWhile0 (flip (<=) (Neg (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) otherwise",fontsize=16,color="black",shape="box"];123 -> 144[label="",style="solid", color="black", weight=3];
124[label="takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];124 -> 145[label="",style="solid", color="black", weight=3];
886 -> 789[label="",style="dashed", color="red", weight=0];
886[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (primCmpNat wv520 wv530 == GT))",fontsize=16,color="magenta"];886 -> 894[label="",style="dashed", color="magenta", weight=3];
886 -> 895[label="",style="dashed", color="magenta", weight=3];
887[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (GT == GT))",fontsize=16,color="black",shape="box"];887 -> 896[label="",style="solid", color="black", weight=3];
888[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (LT == GT))",fontsize=16,color="black",shape="box"];888 -> 897[label="",style="solid", color="black", weight=3];
889[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not (EQ == GT))",fontsize=16,color="black",shape="box"];889 -> 898[label="",style="solid", color="black", weight=3];
130[label="takeWhile0 (flip (<=) (Pos Zero)) (Pos (Succ wv3000)) (numericEnumFrom $! Pos (Succ wv3000) + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];130 -> 153[label="",style="solid", color="black", weight=3];
131[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (numericEnumFrom $! Pos Zero + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];131 -> 154[label="",style="solid", color="black", weight=3];
132[label="takeWhile (flip (<=) (Pos Zero)) (Pos Zero + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Pos Zero + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];132 -> 155[label="",style="solid", color="black", weight=3];
133[label="[]",fontsize=16,color="green",shape="box"];134[label="takeWhile (flip (<=) (Neg Zero)) (Pos Zero + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Pos Zero + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];134 -> 156[label="",style="solid", color="black", weight=3];
135[label="takeWhile (flip (<=) (Pos wv310)) (enforceWHNF (WHNF (Neg (Succ wv3000) + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Neg (Succ wv3000) + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];135 -> 157[label="",style="solid", color="black", weight=3];
890 -> 835[label="",style="dashed", color="red", weight=0];
890[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (primCmpNat wv570 wv580 == GT))",fontsize=16,color="magenta"];890 -> 899[label="",style="dashed", color="magenta", weight=3];
890 -> 900[label="",style="dashed", color="magenta", weight=3];
891[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (GT == GT))",fontsize=16,color="black",shape="box"];891 -> 901[label="",style="solid", color="black", weight=3];
892[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (LT == GT))",fontsize=16,color="black",shape="box"];892 -> 902[label="",style="solid", color="black", weight=3];
893[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not (EQ == GT))",fontsize=16,color="black",shape="box"];893 -> 903[label="",style="solid", color="black", weight=3];
141[label="takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom $! Neg (Succ wv3000) + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];141 -> 165[label="",style="solid", color="black", weight=3];
142[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (Neg Zero + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Neg Zero + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];142 -> 166[label="",style="solid", color="black", weight=3];
143[label="takeWhile (flip (<=) (Pos Zero)) (Neg Zero + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Neg Zero + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];143 -> 167[label="",style="solid", color="black", weight=3];
144[label="takeWhile0 (flip (<=) (Neg (Succ wv3100))) (Neg Zero) (numericEnumFrom $! Neg Zero + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];144 -> 168[label="",style="solid", color="black", weight=3];
145[label="takeWhile (flip (<=) (Neg Zero)) (Neg Zero + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Neg Zero + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];145 -> 169[label="",style="solid", color="black", weight=3];
894[label="wv530",fontsize=16,color="green",shape="box"];895[label="wv520",fontsize=16,color="green",shape="box"];896[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not True)",fontsize=16,color="black",shape="box"];896 -> 904[label="",style="solid", color="black", weight=3];
897[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="triangle"];897 -> 905[label="",style="solid", color="black", weight=3];
898 -> 897[label="",style="dashed", color="red", weight=0];
898[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="magenta"];153[label="[]",fontsize=16,color="green",shape="box"];154[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (Pos Zero + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Pos Zero + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];154 -> 177[label="",style="solid", color="black", weight=3];
155[label="takeWhile (flip (<=) (Pos Zero)) (enforceWHNF (WHNF (Pos Zero + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Pos Zero + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];155 -> 178[label="",style="solid", color="black", weight=3];
156[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (Pos Zero + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Pos Zero + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];156 -> 179[label="",style="solid", color="black", weight=3];
157[label="takeWhile (flip (<=) (Pos wv310)) (enforceWHNF (WHNF (primPlusInt (Neg (Succ wv3000)) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Neg (Succ wv3000)) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];157 -> 180[label="",style="solid", color="black", weight=3];
899[label="wv580",fontsize=16,color="green",shape="box"];900[label="wv570",fontsize=16,color="green",shape="box"];901[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not True)",fontsize=16,color="black",shape="box"];901 -> 906[label="",style="solid", color="black", weight=3];
902[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="black",shape="triangle"];902 -> 907[label="",style="solid", color="black", weight=3];
903 -> 902[label="",style="dashed", color="red", weight=0];
903[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) (not False)",fontsize=16,color="magenta"];165[label="takeWhile (flip (<=) (Neg Zero)) (Neg (Succ wv3000) + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Neg (Succ wv3000) + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];165 -> 188[label="",style="solid", color="black", weight=3];
166[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (enforceWHNF (WHNF (Neg Zero + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Neg Zero + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];166 -> 189[label="",style="solid", color="black", weight=3];
167[label="takeWhile (flip (<=) (Pos Zero)) (enforceWHNF (WHNF (Neg Zero + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Neg Zero + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];167 -> 190[label="",style="solid", color="black", weight=3];
168[label="[]",fontsize=16,color="green",shape="box"];169[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (Neg Zero + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Neg Zero + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];169 -> 191[label="",style="solid", color="black", weight=3];
904[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) False",fontsize=16,color="black",shape="box"];904 -> 908[label="",style="solid", color="black", weight=3];
905[label="takeWhile1 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];905 -> 909[label="",style="solid", color="black", weight=3];
177[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (enforceWHNF (WHNF (Pos Zero + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Pos Zero + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];177 -> 200[label="",style="solid", color="black", weight=3];
178[label="takeWhile (flip (<=) (Pos Zero)) (enforceWHNF (WHNF (primPlusInt (Pos Zero) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Pos Zero) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];178 -> 201[label="",style="solid", color="black", weight=3];
179[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primPlusInt (Pos Zero) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Pos Zero) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];179 -> 202[label="",style="solid", color="black", weight=3];
180[label="takeWhile (flip (<=) (Pos wv310)) (enforceWHNF (WHNF (primPlusInt (Neg (Succ wv3000)) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Neg (Succ wv3000)) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];180 -> 203[label="",style="solid", color="black", weight=3];
906[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) False",fontsize=16,color="black",shape="box"];906 -> 910[label="",style="solid", color="black", weight=3];
907[label="takeWhile1 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];907 -> 911[label="",style="solid", color="black", weight=3];
188[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (Neg (Succ wv3000) + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Neg (Succ wv3000) + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];188 -> 212[label="",style="solid", color="black", weight=3];
189[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (enforceWHNF (WHNF (primPlusInt (Neg Zero) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Neg Zero) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];189 -> 213[label="",style="solid", color="black", weight=3];
190[label="takeWhile (flip (<=) (Pos Zero)) (enforceWHNF (WHNF (primPlusInt (Neg Zero) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Neg Zero) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];190 -> 214[label="",style="solid", color="black", weight=3];
191[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primPlusInt (Neg Zero) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Neg Zero) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];191 -> 215[label="",style="solid", color="black", weight=3];
908[label="takeWhile0 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) otherwise",fontsize=16,color="black",shape="box"];908 -> 912[label="",style="solid", color="black", weight=3];
909[label="Pos (Succ wv51) : takeWhile (flip (<=) (Pos (Succ wv50))) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];909 -> 913[label="",style="dashed", color="green", weight=3];
200[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (enforceWHNF (WHNF (primPlusInt (Pos Zero) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Pos Zero) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];200 -> 226[label="",style="solid", color="black", weight=3];
201[label="takeWhile (flip (<=) (Pos Zero)) (enforceWHNF (WHNF (primPlusInt (Pos Zero) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Pos Zero) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];201 -> 227[label="",style="solid", color="black", weight=3];
202[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primPlusInt (Pos Zero) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Pos Zero) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];202 -> 228[label="",style="solid", color="black", weight=3];
203[label="takeWhile (flip (<=) (Pos wv310)) (enforceWHNF (WHNF (primMinusNat (Succ Zero) (Succ wv3000))) (numericEnumFrom (primMinusNat (Succ Zero) (Succ wv3000))))",fontsize=16,color="black",shape="box"];203 -> 229[label="",style="solid", color="black", weight=3];
910[label="takeWhile0 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) otherwise",fontsize=16,color="black",shape="box"];910 -> 914[label="",style="solid", color="black", weight=3];
911[label="Neg (Succ wv56) : takeWhile (flip (<=) (Neg (Succ wv55))) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero)))",fontsize=16,color="green",shape="box"];911 -> 915[label="",style="dashed", color="green", weight=3];
212[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primPlusInt (Neg (Succ wv3000)) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Neg (Succ wv3000)) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];212 -> 240[label="",style="solid", color="black", weight=3];
213[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (enforceWHNF (WHNF (primPlusInt (Neg Zero) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Neg Zero) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];213 -> 241[label="",style="solid", color="black", weight=3];
214[label="takeWhile (flip (<=) (Pos Zero)) (enforceWHNF (WHNF (primPlusInt (Neg Zero) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Neg Zero) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];214 -> 242[label="",style="solid", color="black", weight=3];
215[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primPlusInt (Neg Zero) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Neg Zero) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];215 -> 243[label="",style="solid", color="black", weight=3];
912[label="takeWhile0 (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51)) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];912 -> 916[label="",style="solid", color="black", weight=3];
913[label="takeWhile (flip (<=) (Pos (Succ wv50))) (numericEnumFrom $! Pos (Succ wv51) + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];913 -> 917[label="",style="solid", color="black", weight=3];
226[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (enforceWHNF (WHNF (primPlusInt (Pos Zero) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Pos Zero) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];226 -> 253[label="",style="solid", color="black", weight=3];
227[label="takeWhile (flip (<=) (Pos Zero)) (enforceWHNF (WHNF (Pos (primPlusNat Zero (Succ Zero)))) (numericEnumFrom (Pos (primPlusNat Zero (Succ Zero)))))",fontsize=16,color="black",shape="box"];227 -> 254[label="",style="solid", color="black", weight=3];
228[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (Pos (primPlusNat Zero (Succ Zero)))) (numericEnumFrom (Pos (primPlusNat Zero (Succ Zero)))))",fontsize=16,color="black",shape="box"];228 -> 255[label="",style="solid", color="black", weight=3];
229[label="takeWhile (flip (<=) (Pos wv310)) (enforceWHNF (WHNF (primMinusNat Zero wv3000)) (numericEnumFrom (primMinusNat Zero wv3000)))",fontsize=16,color="burlywood",shape="box"];994[label="wv3000/Succ wv30000",fontsize=10,color="white",style="solid",shape="box"];229 -> 994[label="",style="solid", color="burlywood", weight=9];
994 -> 256[label="",style="solid", color="burlywood", weight=3];
995[label="wv3000/Zero",fontsize=10,color="white",style="solid",shape="box"];229 -> 995[label="",style="solid", color="burlywood", weight=9];
995 -> 257[label="",style="solid", color="burlywood", weight=3];
914[label="takeWhile0 (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56)) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero))) True",fontsize=16,color="black",shape="box"];914 -> 918[label="",style="solid", color="black", weight=3];
915[label="takeWhile (flip (<=) (Neg (Succ wv55))) (numericEnumFrom $! Neg (Succ wv56) + fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];915 -> 919[label="",style="solid", color="black", weight=3];
240[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primPlusInt (Neg (Succ wv3000)) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Neg (Succ wv3000)) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];240 -> 267[label="",style="solid", color="black", weight=3];
241[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (enforceWHNF (WHNF (primMinusNat (Succ Zero) Zero)) (numericEnumFrom (primMinusNat (Succ Zero) Zero)))",fontsize=16,color="black",shape="box"];241 -> 268[label="",style="solid", color="black", weight=3];
242[label="takeWhile (flip (<=) (Pos Zero)) (enforceWHNF (WHNF (primMinusNat (Succ Zero) Zero)) (numericEnumFrom (primMinusNat (Succ Zero) Zero)))",fontsize=16,color="black",shape="box"];242 -> 269[label="",style="solid", color="black", weight=3];
243[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primMinusNat (Succ Zero) Zero)) (numericEnumFrom (primMinusNat (Succ Zero) Zero)))",fontsize=16,color="black",shape="box"];243 -> 270[label="",style="solid", color="black", weight=3];
916[label="[]",fontsize=16,color="green",shape="box"];917[label="takeWhile (flip (<=) (Pos (Succ wv50))) (Pos (Succ wv51) + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Pos (Succ wv51) + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];917 -> 920[label="",style="solid", color="black", weight=3];
253[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (enforceWHNF (WHNF (Pos (primPlusNat Zero (Succ Zero)))) (numericEnumFrom (Pos (primPlusNat Zero (Succ Zero)))))",fontsize=16,color="black",shape="box"];253 -> 281[label="",style="solid", color="black", weight=3];
254 -> 7[label="",style="dashed", color="red", weight=0];
254[label="takeWhile (flip (<=) (Pos Zero)) (numericEnumFrom (Pos (primPlusNat Zero (Succ Zero))))",fontsize=16,color="magenta"];254 -> 282[label="",style="dashed", color="magenta", weight=3];
254 -> 283[label="",style="dashed", color="magenta", weight=3];
255 -> 7[label="",style="dashed", color="red", weight=0];
255[label="takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom (Pos (primPlusNat Zero (Succ Zero))))",fontsize=16,color="magenta"];255 -> 284[label="",style="dashed", color="magenta", weight=3];
255 -> 285[label="",style="dashed", color="magenta", weight=3];
256[label="takeWhile (flip (<=) (Pos wv310)) (enforceWHNF (WHNF (primMinusNat Zero (Succ wv30000))) (numericEnumFrom (primMinusNat Zero (Succ wv30000))))",fontsize=16,color="black",shape="box"];256 -> 286[label="",style="solid", color="black", weight=3];
257[label="takeWhile (flip (<=) (Pos wv310)) (enforceWHNF (WHNF (primMinusNat Zero Zero)) (numericEnumFrom (primMinusNat Zero Zero)))",fontsize=16,color="black",shape="box"];257 -> 287[label="",style="solid", color="black", weight=3];
918[label="[]",fontsize=16,color="green",shape="box"];919[label="takeWhile (flip (<=) (Neg (Succ wv55))) (Neg (Succ wv56) + fromInt (Pos (Succ Zero)) `seq` numericEnumFrom (Neg (Succ wv56) + fromInt (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];919 -> 921[label="",style="solid", color="black", weight=3];
267[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primMinusNat (Succ Zero) (Succ wv3000))) (numericEnumFrom (primMinusNat (Succ Zero) (Succ wv3000))))",fontsize=16,color="black",shape="box"];267 -> 298[label="",style="solid", color="black", weight=3];
268[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (enforceWHNF (WHNF (Pos (Succ Zero))) (numericEnumFrom (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];268 -> 299[label="",style="solid", color="black", weight=3];
269[label="takeWhile (flip (<=) (Pos Zero)) (enforceWHNF (WHNF (Pos (Succ Zero))) (numericEnumFrom (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];269 -> 300[label="",style="solid", color="black", weight=3];
270[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (Pos (Succ Zero))) (numericEnumFrom (Pos (Succ Zero))))",fontsize=16,color="black",shape="box"];270 -> 301[label="",style="solid", color="black", weight=3];
920[label="takeWhile (flip (<=) (Pos (Succ wv50))) (enforceWHNF (WHNF (Pos (Succ wv51) + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Pos (Succ wv51) + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];920 -> 922[label="",style="solid", color="black", weight=3];
281 -> 7[label="",style="dashed", color="red", weight=0];
281[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (numericEnumFrom (Pos (primPlusNat Zero (Succ Zero))))",fontsize=16,color="magenta"];281 -> 314[label="",style="dashed", color="magenta", weight=3];
281 -> 315[label="",style="dashed", color="magenta", weight=3];
282[label="Pos Zero",fontsize=16,color="green",shape="box"];283[label="Pos (primPlusNat Zero (Succ Zero))",fontsize=16,color="green",shape="box"];283 -> 316[label="",style="dashed", color="green", weight=3];
284[label="Neg Zero",fontsize=16,color="green",shape="box"];285[label="Pos (primPlusNat Zero (Succ Zero))",fontsize=16,color="green",shape="box"];285 -> 317[label="",style="dashed", color="green", weight=3];
286[label="takeWhile (flip (<=) (Pos wv310)) (enforceWHNF (WHNF (Neg (Succ wv30000))) (numericEnumFrom (Neg (Succ wv30000))))",fontsize=16,color="black",shape="box"];286 -> 318[label="",style="solid", color="black", weight=3];
287[label="takeWhile (flip (<=) (Pos wv310)) (enforceWHNF (WHNF (Pos Zero)) (numericEnumFrom (Pos Zero)))",fontsize=16,color="black",shape="box"];287 -> 319[label="",style="solid", color="black", weight=3];
921[label="takeWhile (flip (<=) (Neg (Succ wv55))) (enforceWHNF (WHNF (Neg (Succ wv56) + fromInt (Pos (Succ Zero)))) (numericEnumFrom (Neg (Succ wv56) + fromInt (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];921 -> 923[label="",style="solid", color="black", weight=3];
298[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primMinusNat Zero wv3000)) (numericEnumFrom (primMinusNat Zero wv3000)))",fontsize=16,color="burlywood",shape="box"];999[label="wv3000/Succ wv30000",fontsize=10,color="white",style="solid",shape="box"];298 -> 999[label="",style="solid", color="burlywood", weight=9];
999 -> 332[label="",style="solid", color="burlywood", weight=3];
1000[label="wv3000/Zero",fontsize=10,color="white",style="solid",shape="box"];298 -> 1000[label="",style="solid", color="burlywood", weight=9];
1000 -> 333[label="",style="solid", color="burlywood", weight=3];
299 -> 7[label="",style="dashed", color="red", weight=0];
299[label="takeWhile (flip (<=) (Pos (Succ wv3100))) (numericEnumFrom (Pos (Succ Zero)))",fontsize=16,color="magenta"];299 -> 334[label="",style="dashed", color="magenta", weight=3];
299 -> 335[label="",style="dashed", color="magenta", weight=3];
300 -> 7[label="",style="dashed", color="red", weight=0];
300[label="takeWhile (flip (<=) (Pos Zero)) (numericEnumFrom (Pos (Succ Zero)))",fontsize=16,color="magenta"];300 -> 336[label="",style="dashed", color="magenta", weight=3];
300 -> 337[label="",style="dashed", color="magenta", weight=3];
301 -> 7[label="",style="dashed", color="red", weight=0];
301[label="takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom (Pos (Succ Zero)))",fontsize=16,color="magenta"];301 -> 338[label="",style="dashed", color="magenta", weight=3];
301 -> 339[label="",style="dashed", color="magenta", weight=3];
922[label="takeWhile (flip (<=) (Pos (Succ wv50))) (enforceWHNF (WHNF (primPlusInt (Pos (Succ wv51)) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Pos (Succ wv51)) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];922 -> 924[label="",style="solid", color="black", weight=3];
314[label="Pos (Succ wv3100)",fontsize=16,color="green",shape="box"];315[label="Pos (primPlusNat Zero (Succ Zero))",fontsize=16,color="green",shape="box"];315 -> 351[label="",style="dashed", color="green", weight=3];
316[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="black",shape="triangle"];316 -> 352[label="",style="solid", color="black", weight=3];
317 -> 316[label="",style="dashed", color="red", weight=0];
317[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="magenta"];318 -> 7[label="",style="dashed", color="red", weight=0];
318[label="takeWhile (flip (<=) (Pos wv310)) (numericEnumFrom (Neg (Succ wv30000)))",fontsize=16,color="magenta"];318 -> 353[label="",style="dashed", color="magenta", weight=3];
318 -> 354[label="",style="dashed", color="magenta", weight=3];
319 -> 7[label="",style="dashed", color="red", weight=0];
319[label="takeWhile (flip (<=) (Pos wv310)) (numericEnumFrom (Pos Zero))",fontsize=16,color="magenta"];319 -> 355[label="",style="dashed", color="magenta", weight=3];
319 -> 356[label="",style="dashed", color="magenta", weight=3];
923[label="takeWhile (flip (<=) (Neg (Succ wv55))) (enforceWHNF (WHNF (primPlusInt (Neg (Succ wv56)) (fromInt (Pos (Succ Zero))))) (numericEnumFrom (primPlusInt (Neg (Succ wv56)) (fromInt (Pos (Succ Zero))))))",fontsize=16,color="black",shape="box"];923 -> 925[label="",style="solid", color="black", weight=3];
332[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primMinusNat Zero (Succ wv30000))) (numericEnumFrom (primMinusNat Zero (Succ wv30000))))",fontsize=16,color="black",shape="box"];332 -> 368[label="",style="solid", color="black", weight=3];
333[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (primMinusNat Zero Zero)) (numericEnumFrom (primMinusNat Zero Zero)))",fontsize=16,color="black",shape="box"];333 -> 369[label="",style="solid", color="black", weight=3];
334[label="Pos (Succ wv3100)",fontsize=16,color="green",shape="box"];335[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];336[label="Pos Zero",fontsize=16,color="green",shape="box"];337[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];338[label="Neg Zero",fontsize=16,color="green",shape="box"];339[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];924[label="takeWhile (flip (<=) (Pos (Succ wv50))) (enforceWHNF (WHNF (primPlusInt (Pos (Succ wv51)) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Pos (Succ wv51)) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];924 -> 926[label="",style="solid", color="black", weight=3];
351 -> 316[label="",style="dashed", color="red", weight=0];
351[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="magenta"];352[label="Succ Zero",fontsize=16,color="green",shape="box"];353[label="Pos wv310",fontsize=16,color="green",shape="box"];354[label="Neg (Succ wv30000)",fontsize=16,color="green",shape="box"];355[label="Pos wv310",fontsize=16,color="green",shape="box"];356[label="Pos Zero",fontsize=16,color="green",shape="box"];925[label="takeWhile (flip (<=) (Neg (Succ wv55))) (enforceWHNF (WHNF (primPlusInt (Neg (Succ wv56)) (Pos (Succ Zero)))) (numericEnumFrom (primPlusInt (Neg (Succ wv56)) (Pos (Succ Zero)))))",fontsize=16,color="black",shape="box"];925 -> 927[label="",style="solid", color="black", weight=3];
368[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (Neg (Succ wv30000))) (numericEnumFrom (Neg (Succ wv30000))))",fontsize=16,color="black",shape="box"];368 -> 394[label="",style="solid", color="black", weight=3];
369[label="takeWhile (flip (<=) (Neg Zero)) (enforceWHNF (WHNF (Pos Zero)) (numericEnumFrom (Pos Zero)))",fontsize=16,color="black",shape="box"];369 -> 395[label="",style="solid", color="black", weight=3];
926[label="takeWhile (flip (<=) (Pos (Succ wv50))) (enforceWHNF (WHNF (Pos (primPlusNat (Succ wv51) (Succ Zero)))) (numericEnumFrom (Pos (primPlusNat (Succ wv51) (Succ Zero)))))",fontsize=16,color="black",shape="box"];926 -> 928[label="",style="solid", color="black", weight=3];
927[label="takeWhile (flip (<=) (Neg (Succ wv55))) (enforceWHNF (WHNF (primMinusNat (Succ Zero) (Succ wv56))) (numericEnumFrom (primMinusNat (Succ Zero) (Succ wv56))))",fontsize=16,color="black",shape="box"];927 -> 929[label="",style="solid", color="black", weight=3];
394 -> 7[label="",style="dashed", color="red", weight=0];
394[label="takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom (Neg (Succ wv30000)))",fontsize=16,color="magenta"];394 -> 426[label="",style="dashed", color="magenta", weight=3];
394 -> 427[label="",style="dashed", color="magenta", weight=3];
395 -> 7[label="",style="dashed", color="red", weight=0];
395[label="takeWhile (flip (<=) (Neg Zero)) (numericEnumFrom (Pos Zero))",fontsize=16,color="magenta"];395 -> 428[label="",style="dashed", color="magenta", weight=3];
395 -> 429[label="",style="dashed", color="magenta", weight=3];
928 -> 7[label="",style="dashed", color="red", weight=0];
928[label="takeWhile (flip (<=) (Pos (Succ wv50))) (numericEnumFrom (Pos (primPlusNat (Succ wv51) (Succ Zero))))",fontsize=16,color="magenta"];928 -> 930[label="",style="dashed", color="magenta", weight=3];
928 -> 931[label="",style="dashed", color="magenta", weight=3];
929[label="takeWhile (flip (<=) (Neg (Succ wv55))) (enforceWHNF (WHNF (primMinusNat Zero wv56)) (numericEnumFrom (primMinusNat Zero wv56)))",fontsize=16,color="burlywood",shape="box"];1011[label="wv56/Succ wv560",fontsize=10,color="white",style="solid",shape="box"];929 -> 1011[label="",style="solid", color="burlywood", weight=9];
1011 -> 932[label="",style="solid", color="burlywood", weight=3];
1012[label="wv56/Zero",fontsize=10,color="white",style="solid",shape="box"];929 -> 1012[label="",style="solid", color="burlywood", weight=9];
1012 -> 933[label="",style="solid", color="burlywood", weight=3];
426[label="Neg Zero",fontsize=16,color="green",shape="box"];427[label="Neg (Succ wv30000)",fontsize=16,color="green",shape="box"];428[label="Neg Zero",fontsize=16,color="green",shape="box"];429[label="Pos Zero",fontsize=16,color="green",shape="box"];930[label="Pos (Succ wv50)",fontsize=16,color="green",shape="box"];931[label="Pos (primPlusNat (Succ wv51) (Succ Zero))",fontsize=16,color="green",shape="box"];931 -> 934[label="",style="dashed", color="green", weight=3];
932[label="takeWhile (flip (<=) (Neg (Succ wv55))) (enforceWHNF (WHNF (primMinusNat Zero (Succ wv560))) (numericEnumFrom (primMinusNat Zero (Succ wv560))))",fontsize=16,color="black",shape="box"];932 -> 935[label="",style="solid", color="black", weight=3];
933[label="takeWhile (flip (<=) (Neg (Succ wv55))) (enforceWHNF (WHNF (primMinusNat Zero Zero)) (numericEnumFrom (primMinusNat Zero Zero)))",fontsize=16,color="black",shape="box"];933 -> 936[label="",style="solid", color="black", weight=3];
934[label="primPlusNat (Succ wv51) (Succ Zero)",fontsize=16,color="black",shape="box"];934 -> 937[label="",style="solid", color="black", weight=3];
935[label="takeWhile (flip (<=) (Neg (Succ wv55))) (enforceWHNF (WHNF (Neg (Succ wv560))) (numericEnumFrom (Neg (Succ wv560))))",fontsize=16,color="black",shape="box"];935 -> 938[label="",style="solid", color="black", weight=3];
936[label="takeWhile (flip (<=) (Neg (Succ wv55))) (enforceWHNF (WHNF (Pos Zero)) (numericEnumFrom (Pos Zero)))",fontsize=16,color="black",shape="box"];936 -> 939[label="",style="solid", color="black", weight=3];
937[label="Succ (Succ (primPlusNat wv51 Zero))",fontsize=16,color="green",shape="box"];937 -> 940[label="",style="dashed", color="green", weight=3];
938 -> 7[label="",style="dashed", color="red", weight=0];
938[label="takeWhile (flip (<=) (Neg (Succ wv55))) (numericEnumFrom (Neg (Succ wv560)))",fontsize=16,color="magenta"];938 -> 941[label="",style="dashed", color="magenta", weight=3];
938 -> 942[label="",style="dashed", color="magenta", weight=3];
939 -> 7[label="",style="dashed", color="red", weight=0];
939[label="takeWhile (flip (<=) (Neg (Succ wv55))) (numericEnumFrom (Pos Zero))",fontsize=16,color="magenta"];939 -> 943[label="",style="dashed", color="magenta", weight=3];
939 -> 944[label="",style="dashed", color="magenta", weight=3];
940[label="primPlusNat wv51 Zero",fontsize=16,color="burlywood",shape="box"];1015[label="wv51/Succ wv510",fontsize=10,color="white",style="solid",shape="box"];940 -> 1015[label="",style="solid", color="burlywood", weight=9];
1015 -> 945[label="",style="solid", color="burlywood", weight=3];
1016[label="wv51/Zero",fontsize=10,color="white",style="solid",shape="box"];940 -> 1016[label="",style="solid", color="burlywood", weight=9];
1016 -> 946[label="",style="solid", color="burlywood", weight=3];
941[label="Neg (Succ wv55)",fontsize=16,color="green",shape="box"];942[label="Neg (Succ wv560)",fontsize=16,color="green",shape="box"];943[label="Neg (Succ wv55)",fontsize=16,color="green",shape="box"];944[label="Pos Zero",fontsize=16,color="green",shape="box"];945[label="primPlusNat (Succ wv510) Zero",fontsize=16,color="black",shape="box"];945 -> 947[label="",style="solid", color="black", weight=3];
946[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];946 -> 948[label="",style="solid", color="black", weight=3];
947[label="Succ wv510",fontsize=16,color="green",shape="box"];948[label="Zero",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile11(wv55, Succ(wv560), Zero, Succ(wv580)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))
new_takeWhile(Neg(Zero), Neg(Zero)) → new_takeWhile(Neg(Zero), Pos(Succ(Zero)))
new_takeWhile(Pos(Succ(wv3100)), Pos(Succ(wv3000))) → new_takeWhile1(wv3100, wv3000, wv3000, wv3100)
new_takeWhile(Pos(Zero), Pos(Zero)) → new_takeWhile(Pos(Zero), Pos(new_primPlusNat0))
new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000))) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000)
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580)) → new_takeWhile11(wv55, wv56, wv570, wv580)
new_takeWhile1(wv50, wv51, Succ(wv520), Succ(wv530)) → new_takeWhile1(wv50, wv51, wv520, wv530)
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile(Neg(Zero), Neg(Succ(Zero))) → new_takeWhile(Neg(Zero), Pos(Zero))
new_takeWhile(Pos(wv310), Neg(Succ(Succ(wv30000)))) → new_takeWhile(Pos(wv310), Neg(Succ(wv30000)))
new_takeWhile(Neg(Zero), Pos(Zero)) → new_takeWhile(Neg(Zero), Pos(new_primPlusNat0))
new_takeWhile12(wv55, Succ(wv560)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))
new_takeWhile(Pos(Succ(wv3100)), Pos(Zero)) → new_takeWhile(Pos(Succ(wv3100)), Pos(new_primPlusNat0))
new_takeWhile(Pos(Zero), Neg(Zero)) → new_takeWhile(Pos(Zero), Pos(Succ(Zero)))
new_takeWhile1(wv50, wv51, Zero, Succ(wv530)) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile12(wv55, Zero) → new_takeWhile(Neg(Succ(wv55)), Pos(Zero))
new_takeWhile(Neg(Zero), Neg(Succ(Succ(wv30000)))) → new_takeWhile(Neg(Zero), Neg(Succ(wv30000)))
new_takeWhile11(wv55, wv56, Zero, Zero) → new_takeWhile12(wv55, wv56)
new_takeWhile(Pos(wv310), Neg(Succ(Zero))) → new_takeWhile(Pos(wv310), Pos(Zero))
new_takeWhile10(wv50, wv51) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile(Pos(Succ(wv3100)), Neg(Zero)) → new_takeWhile(Pos(Succ(wv3100)), Pos(Succ(Zero)))
new_takeWhile11(wv55, Zero, Zero, Succ(wv580)) → new_takeWhile(Neg(Succ(wv55)), Pos(Zero))

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat0 → Succ(Zero)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 10 less nodes.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Zero), Neg(Succ(Succ(wv30000)))) → new_takeWhile(Neg(Zero), Neg(Succ(wv30000)))

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat0 → Succ(Zero)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Zero), Neg(Succ(Succ(wv30000)))) → new_takeWhile(Neg(Zero), Neg(Succ(wv30000)))

R is empty.
The set Q consists of the following terms:

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ RuleRemovalProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Zero), Neg(Succ(Succ(wv30000)))) → new_takeWhile(Neg(Zero), Neg(Succ(wv30000)))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_takeWhile(Neg(Zero), Neg(Succ(Succ(wv30000)))) → new_takeWhile(Neg(Zero), Neg(Succ(wv30000)))

Used ordering: POLO with Polynomial interpretation [25]:

POL(Neg(x₁)) = 2·x₁
POL(Succ(x₁)) = 1 + 2·x₁
POL(Zero) = 0
POL(new_takeWhile(x₁, x₂)) = x₁ + 2·x₂

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ RuleRemovalProof

                                  ↳ QDP

                                    ↳ PisEmptyProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(Succ(wv3100)), Pos(Succ(wv3000))) → new_takeWhile1(wv3100, wv3000, wv3000, wv3100)
new_takeWhile1(wv50, wv51, Zero, Succ(wv530)) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile10(wv50, wv51) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile1(wv50, wv51, Succ(wv520), Succ(wv530)) → new_takeWhile1(wv50, wv51, wv520, wv530)

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat0 → Succ(Zero)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(Succ(wv3100)), Pos(Succ(wv3000))) → new_takeWhile1(wv3100, wv3000, wv3000, wv3100)
new_takeWhile1(wv50, wv51, Zero, Succ(wv530)) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile10(wv50, wv51) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile1(wv50, wv51, Succ(wv520), Succ(wv530)) → new_takeWhile1(wv50, wv51, wv520, wv530)

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(Succ(wv3100)), Pos(Succ(wv3000))) → new_takeWhile1(wv3100, wv3000, wv3000, wv3100)
new_takeWhile1(wv50, wv51, Zero, Succ(wv530)) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile10(wv50, wv51) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile1(wv50, wv51, Succ(wv520), Succ(wv530)) → new_takeWhile1(wv50, wv51, wv520, wv530)
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule new_takeWhile(Pos(Succ(wv3100)), Pos(Succ(wv3000))) → new_takeWhile1(wv3100, wv3000, wv3000, wv3100) we obtained the following new rules:

new_takeWhile(Pos(Succ(z0)), Pos(Succ(Succ(y_0)))) → new_takeWhile1(z0, Succ(y_0), Succ(y_0), z0)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(wv50, wv51, Zero, Succ(wv530)) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile(Pos(Succ(z0)), Pos(Succ(Succ(y_0)))) → new_takeWhile1(z0, Succ(y_0), Succ(y_0), z0)
new_takeWhile10(wv50, wv51) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile1(wv50, wv51, Succ(wv520), Succ(wv530)) → new_takeWhile1(wv50, wv51, wv520, wv530)

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_takeWhile1(wv50, wv51, Succ(wv520), Succ(wv530)) → new_takeWhile1(wv50, wv51, wv520, wv530) we obtained the following new rules:

new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(wv50, wv51, Zero, Succ(wv530)) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile(Pos(Succ(z0)), Pos(Succ(Succ(y_0)))) → new_takeWhile1(z0, Succ(y_0), Succ(y_0), z0)
new_takeWhile10(wv50, wv51) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_takeWhile(Pos(Succ(z0)), Pos(Succ(Succ(y_0)))) → new_takeWhile1(z0, Succ(y_0), Succ(y_0), z0) we obtained the following new rules:

new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile1(wv50, wv51, Zero, Succ(wv530)) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(wv50, wv51) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule new_takeWhile1(wv50, wv51, Zero, Succ(wv530)) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51))))) at position [1,0,0,0] we obtained the following new rules:

new_takeWhile1(y0, Succ(x0), Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(y0, Zero, Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(y0, Zero, Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(y0, Succ(x0), Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(wv50, wv51) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51)))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule new_takeWhile10(wv50, wv51) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51))))) at position [1,0,0,0] we obtained the following new rules:

new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile10(y0, Succ(x0)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(y0, Zero, Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile10(y0, Succ(x0)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile1(y0, Succ(x0), Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(y0, Zero, Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile10(y0, Succ(x0)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(y0, Succ(x0), Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))

R is empty.
The set Q consists of the following terms:

new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(y0, Zero, Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile10(y0, Succ(x0)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile1(y0, Succ(x0), Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_takeWhile1(y0, Zero, Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero)))) we obtained the following new rules:

new_takeWhile1(Succ(Zero), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero))))
new_takeWhile1(Succ(Succ(y_0)), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                                                              ↳ QDP

                                                                ↳ ForwardInstantiation

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(Succ(Zero), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile10(y0, Succ(x0)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(Succ(Succ(y_0)), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile1(y0, Succ(x0), Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_takeWhile10(y0, Succ(x0)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0))))) we obtained the following new rules:

new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                                                              ↳ QDP

                                                                ↳ ForwardInstantiation

                                                                  ↳ QDP

                                                                    ↳ ForwardInstantiation

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(Succ(Zero), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(Succ(Succ(y_0)), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(y0, Succ(x0), Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0)))))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_takeWhile1(y0, Succ(x0), Zero, Succ(y2)) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Succ(x0))))) we obtained the following new rules:

new_takeWhile1(Succ(Succ(y_0)), Succ(x1), Zero, Succ(x2)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                                                              ↳ QDP

                                                                ↳ ForwardInstantiation

                                                                  ↳ QDP

                                                                    ↳ ForwardInstantiation

                                                                      ↳ QDP

                                                                        ↳ ForwardInstantiation

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(Succ(Zero), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(Succ(Succ(y_0)), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))
new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51)
new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile1(Succ(Succ(y_0)), Succ(x1), Zero, Succ(x2)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_takeWhile1(wv50, wv51, Zero, Zero) → new_takeWhile10(wv50, wv51) we obtained the following new rules:

new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero) → new_takeWhile10(Succ(Succ(y_0)), Succ(y_1))
new_takeWhile1(x0, Zero, Zero, Zero) → new_takeWhile10(x0, Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                                                              ↳ QDP

                                                                ↳ ForwardInstantiation

                                                                  ↳ QDP

                                                                    ↳ ForwardInstantiation

                                                                      ↳ QDP

                                                                        ↳ ForwardInstantiation

                                                                          ↳ QDP

                                                                            ↳ ForwardInstantiation

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(Succ(Zero), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(Succ(Succ(y_0)), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))
new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero) → new_takeWhile10(Succ(Succ(y_0)), Succ(y_1))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(x0, Zero, Zero, Zero) → new_takeWhile10(x0, Zero)
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile1(Succ(Succ(y_0)), Succ(x1), Zero, Succ(x2)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_takeWhile1(x0, x1, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, x1, Zero, Zero) we obtained the following new rules:

new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Succ(Zero), Succ(Zero)) → new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero)
new_takeWhile1(x0, Zero, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, Zero, Zero, Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                                                              ↳ QDP

                                                                ↳ ForwardInstantiation

                                                                  ↳ QDP

                                                                    ↳ ForwardInstantiation

                                                                      ↳ QDP

                                                                        ↳ ForwardInstantiation

                                                                          ↳ QDP

                                                                            ↳ ForwardInstantiation

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(Succ(Zero), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(Succ(Succ(y_0)), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))
new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile1(x0, Zero, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, Zero, Zero, Zero)
new_takeWhile(Pos(Succ(Succ(Zero))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Zero), Succ(Zero), Succ(Zero), Succ(Zero))
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero) → new_takeWhile10(Succ(Succ(y_0)), Succ(y_1))
new_takeWhile1(x0, Zero, Zero, Zero) → new_takeWhile10(x0, Zero)
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Succ(Zero), Succ(Zero)) → new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero)
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile1(Succ(Succ(y_0)), Succ(x1), Zero, Succ(x2)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                                                              ↳ QDP

                                                                ↳ ForwardInstantiation

                                                                  ↳ QDP

                                                                    ↳ ForwardInstantiation

                                                                      ↳ QDP

                                                                        ↳ ForwardInstantiation

                                                                          ↳ QDP

                                                                            ↳ ForwardInstantiation

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ ForwardInstantiation

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero) → new_takeWhile10(Succ(Succ(y_0)), Succ(y_1))
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(x0, Zero, Zero, Zero) → new_takeWhile10(x0, Zero)
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Succ(Zero), Succ(Zero)) → new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero)
new_takeWhile1(Succ(Succ(y_0)), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero))))
new_takeWhile1(x0, Zero, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, Zero, Zero, Zero)
new_takeWhile1(Succ(Succ(y_0)), Succ(x1), Zero, Succ(x2)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_takeWhile10(y0, Zero) → new_takeWhile(Pos(Succ(y0)), Pos(Succ(Succ(Zero)))) we obtained the following new rules:

new_takeWhile10(Succ(Succ(y_0)), Zero) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                                                              ↳ QDP

                                                                ↳ ForwardInstantiation

                                                                  ↳ QDP

                                                                    ↳ ForwardInstantiation

                                                                      ↳ QDP

                                                                        ↳ ForwardInstantiation

                                                                          ↳ QDP

                                                                            ↳ ForwardInstantiation

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ ForwardInstantiation

                                                                                      ↳ QDP

                                                                                        ↳ QDPOrderProof

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile10(Succ(Succ(y_0)), Zero) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(Succ(Succ(y_0)), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))
new_takeWhile1(x0, Zero, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, Zero, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero) → new_takeWhile10(Succ(Succ(y_0)), Succ(y_1))
new_takeWhile1(x0, Zero, Zero, Zero) → new_takeWhile10(x0, Zero)
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Succ(Zero), Succ(Zero)) → new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero)
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile1(Succ(Succ(y_0)), Succ(x1), Zero, Succ(x2)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_takeWhile10(Succ(Succ(y_0)), Zero) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))
new_takeWhile1(Succ(Succ(y_0)), Zero, Zero, Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Zero))))

The remaining pairs can at least be oriented weakly.

new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(x0, Zero, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, Zero, Zero, Zero)
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero) → new_takeWhile10(Succ(Succ(y_0)), Succ(y_1))
new_takeWhile1(x0, Zero, Zero, Zero) → new_takeWhile10(x0, Zero)
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Succ(Zero), Succ(Zero)) → new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero)
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile1(Succ(Succ(y_0)), Succ(x1), Zero, Succ(x2)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))

Used ordering: Polynomial interpretation [25]:

POL(Pos(x₁)) = 0
POL(Succ(x₁)) = 0
POL(Zero) = 1
POL(new_takeWhile(x₁, x₂)) = 0
POL(new_takeWhile1(x₁, x₂, x₃, x₄)) = x₁ + x₂
POL(new_takeWhile10(x₁, x₂)) = x₂

The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                                                              ↳ QDP

                                                                ↳ ForwardInstantiation

                                                                  ↳ QDP

                                                                    ↳ ForwardInstantiation

                                                                      ↳ QDP

                                                                        ↳ ForwardInstantiation

                                                                          ↳ QDP

                                                                            ↳ ForwardInstantiation

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ ForwardInstantiation

                                                                                      ↳ QDP

                                                                                        ↳ QDPOrderProof

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero) → new_takeWhile10(Succ(Succ(y_0)), Succ(y_1))
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile(Pos(Succ(Succ(Succ(y_2)))), Pos(Succ(Succ(Zero)))) → new_takeWhile1(Succ(Succ(y_2)), Succ(Zero), Succ(Zero), Succ(Succ(y_2)))
new_takeWhile1(x0, Zero, Zero, Zero) → new_takeWhile10(x0, Zero)
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Succ(Zero), Succ(Zero)) → new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero)
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile1(Succ(Succ(y_0)), Succ(x1), Zero, Succ(x2)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile1(x0, Zero, Succ(Zero), Succ(Zero)) → new_takeWhile1(x0, Zero, Zero, Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ ForwardInstantiation

                                      ↳ QDP

                                        ↳ ForwardInstantiation

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ Narrowing

                                                  ↳ QDP

                                                    ↳ UsableRulesProof

                                                      ↳ QDP

                                                        ↳ QReductionProof

                                                          ↳ QDP

                                                            ↳ ForwardInstantiation

                                                              ↳ QDP

                                                                ↳ ForwardInstantiation

                                                                  ↳ QDP

                                                                    ↳ ForwardInstantiation

                                                                      ↳ QDP

                                                                        ↳ ForwardInstantiation

                                                                          ↳ QDP

                                                                            ↳ ForwardInstantiation

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ ForwardInstantiation

                                                                                      ↳ QDP

                                                                                        ↳ QDPOrderProof

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

                                                                                              ↳ QDP

                      ↳ QDP

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero) → new_takeWhile10(Succ(Succ(y_0)), Succ(y_1))
new_takeWhile1(x0, x1, Succ(Succ(y_2)), Succ(Succ(y_3))) → new_takeWhile1(x0, x1, Succ(y_2), Succ(y_3))
new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Succ(Zero), Succ(Zero)) → new_takeWhile1(Succ(Succ(y_0)), Succ(y_1), Zero, Zero)
new_takeWhile1(x0, x1, Succ(Zero), Succ(Succ(y_2))) → new_takeWhile1(x0, x1, Zero, Succ(y_2))
new_takeWhile10(Succ(Succ(y_0)), Succ(x1)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))
new_takeWhile(Pos(Succ(Succ(Succ(y_3)))), Pos(Succ(Succ(Succ(y_2))))) → new_takeWhile1(Succ(Succ(y_3)), Succ(Succ(y_2)), Succ(Succ(y_2)), Succ(Succ(y_3)))
new_takeWhile1(Succ(Succ(y_0)), Succ(x1), Zero, Succ(x2)) → new_takeWhile(Pos(Succ(Succ(Succ(y_0)))), Pos(Succ(Succ(Succ(x1)))))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(wv310), Neg(Succ(Succ(wv30000)))) → new_takeWhile(Pos(wv310), Neg(Succ(wv30000)))

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat0 → Succ(Zero)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(wv310), Neg(Succ(Succ(wv30000)))) → new_takeWhile(Pos(wv310), Neg(Succ(wv30000)))

R is empty.
The set Q consists of the following terms:

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ RuleRemovalProof

                      ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(wv310), Neg(Succ(Succ(wv30000)))) → new_takeWhile(Pos(wv310), Neg(Succ(wv30000)))

Used ordering: POLO with Polynomial interpretation [25]:

POL(Neg(x₁)) = 2·x₁
POL(Pos(x₁)) = x₁
POL(Succ(x₁)) = 1 + 2·x₁
POL(new_takeWhile(x₁, x₂)) = x₁ + 2·x₂

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ RuleRemovalProof

                                  ↳ QDP

                                    ↳ PisEmptyProof

                      ↳ QDP

              ↳ Narrow

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile11(wv55, Succ(wv560), Zero, Succ(wv580)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))
new_takeWhile12(wv55, Succ(wv560)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))
new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000))) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000)
new_takeWhile11(wv55, wv56, Zero, Zero) → new_takeWhile12(wv55, wv56)
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580)) → new_takeWhile11(wv55, wv56, wv570, wv580)

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510)) → Succ(wv510)
new_primPlusNat0 → Succ(Zero)
new_primPlusNat(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile11(wv55, Succ(wv560), Zero, Succ(wv580)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))
new_takeWhile12(wv55, Succ(wv560)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))
new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000))) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000)
new_takeWhile11(wv55, wv56, Zero, Zero) → new_takeWhile12(wv55, wv56)
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580)) → new_takeWhile11(wv55, wv56, wv570, wv580)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ QDPOrderProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile11(wv55, Succ(wv560), Zero, Succ(wv580)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))
new_takeWhile12(wv55, Succ(wv560)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))
new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000))) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000)
new_takeWhile11(wv55, wv56, Zero, Zero) → new_takeWhile12(wv55, wv56)
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580)) → new_takeWhile11(wv55, wv56, wv570, wv580)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_takeWhile11(wv55, Succ(wv560), Zero, Succ(wv580)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))
new_takeWhile12(wv55, Succ(wv560)) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)))

The remaining pairs can at least be oriented weakly.

new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000))) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000)
new_takeWhile11(wv55, wv56, Zero, Zero) → new_takeWhile12(wv55, wv56)
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580)) → new_takeWhile11(wv55, wv56, wv570, wv580)

Used ordering: Polynomial interpretation [25]:

POL(Neg(x₁)) = x₁
POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_takeWhile(x₁, x₂)) = x₂
POL(new_takeWhile11(x₁, x₂, x₃, x₄)) = 1 + x₂
POL(new_takeWhile12(x₁, x₂)) = 1 + x₂

The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ DependencyGraphProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000))) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000)
new_takeWhile11(wv55, wv56, Zero, Zero) → new_takeWhile12(wv55, wv56)
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580)) → new_takeWhile11(wv55, wv56, wv570, wv580)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ QReductionProof

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPSizeChangeProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580)) → new_takeWhile11(wv55, wv56, wv570, wv580)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580)) → new_takeWhile11(wv55, wv56, wv570, wv580)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

Haskell To QDPs

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Zero), Neg(Succ(Zero)), []) → new_takeWhile(Neg(Zero), Pos(Zero), [])
new_takeWhile(Neg(Zero), Neg(Succ(Succ(wv30000))), []) → new_takeWhile(Neg(Zero), Neg(Succ(wv30000)), [])
new_takeWhile(Neg(Zero), Pos(Zero), []) → new_takeWhile(Neg(Zero), Pos(new_primPlusNat0([])), [])
new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000)), []) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000, [])
new_takeWhile11(wv55, wv56, Zero, Zero, []) → new_takeWhile12(wv55, wv56, [])
new_takeWhile12(wv55, Succ(wv560), []) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)), [])
new_takeWhile11(wv55, Zero, Zero, Succ(wv580), []) → new_takeWhile(Neg(Succ(wv55)), Pos(Zero), [])
new_takeWhile11(wv55, Succ(wv560), Zero, Succ(wv580), []) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)), [])
new_takeWhile1(wv50, wv51, Succ(wv520), Succ(wv530), []) → new_takeWhile1(wv50, wv51, wv520, wv530, [])
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580), []) → new_takeWhile11(wv55, wv56, wv570, wv580, [])
new_takeWhile(Pos(Succ(wv3100)), Neg(Zero), []) → new_takeWhile(Pos(Succ(wv3100)), Pos(Succ(Zero)), [])
new_takeWhile(Pos(wv310), Neg(Succ(Succ(wv30000))), []) → new_takeWhile(Pos(wv310), Neg(Succ(wv30000)), [])
new_takeWhile(Pos(Succ(wv3100)), Pos(Succ(wv3000)), []) → new_takeWhile1(wv3100, wv3000, wv3000, wv3100, [])
new_takeWhile(Pos(Zero), Pos(Zero), []) → new_takeWhile(Pos(Zero), Pos(new_primPlusNat0([])), [])
new_takeWhile1(wv50, wv51, Zero, Zero, []) → new_takeWhile10(wv50, wv51, [])
new_takeWhile(Pos(Succ(wv3100)), Pos(Zero), []) → new_takeWhile(Pos(Succ(wv3100)), Pos(new_primPlusNat0([])), [])
new_takeWhile(Pos(wv310), Neg(Succ(Zero)), []) → new_takeWhile(Pos(wv310), Pos(Zero), [])
new_takeWhile1(wv50, wv51, Zero, Succ(wv530), []) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51, [])))), [])
new_takeWhile(Neg(Zero), Neg(Zero), []) → new_takeWhile(Neg(Zero), Pos(Succ(Zero)), [])
new_takeWhile10(wv50, wv51, []) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51, [])))), [])
new_takeWhile(Pos(Zero), Neg(Zero), []) → new_takeWhile(Pos(Zero), Pos(Succ(Zero)), [])
new_takeWhile12(wv55, Zero, []) → new_takeWhile(Neg(Succ(wv55)), Pos(Zero), [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Q is empty.
We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 7 SCCs with 7 less nodes.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ RuleRemovalProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(Zero), Pos(Zero), []) → new_takeWhile(Pos(Zero), Pos(new_primPlusNat0([])), [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Q is empty.
We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

new_primPlusNat(Zero, []) → Zero

Used ordering: POLO with Polynomial interpretation [25]:

POL(Pos(x₁)) = x₁
POL(Succ(x₁)) = x₁
POL(Zero) = 1
POL([]) = 0
POL(new_primPlusNat(x₁, x₂)) = 2·x₁ + 2·x₂
POL(new_primPlusNat0(x₁)) = 1 + 2·x₁
POL(new_takeWhile(x₁, x₂, x₃)) = x₁ + x₂ + x₃

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(Zero), Pos(Zero), []) → new_takeWhile(Pos(Zero), Pos(new_primPlusNat0([])), [])

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Q is empty.
We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(Succ(wv3100)), Pos(Succ(wv3000)), []) → new_takeWhile1(wv3100, wv3000, wv3000, wv3100, [])
new_takeWhile1(wv50, wv51, Zero, Zero, []) → new_takeWhile10(wv50, wv51, [])
new_takeWhile1(wv50, wv51, Succ(wv520), Succ(wv530), []) → new_takeWhile1(wv50, wv51, wv520, wv530, [])
new_takeWhile1(wv50, wv51, Zero, Succ(wv530), []) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51, [])))), [])
new_takeWhile10(wv50, wv51, []) → new_takeWhile(Pos(Succ(wv50)), Pos(Succ(Succ(new_primPlusNat(wv51, [])))), [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Q is empty.
We have to consider all (P,Q,R)-chains.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ RuleRemovalProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(Succ(wv3100)), Pos(Zero), []) → new_takeWhile(Pos(Succ(wv3100)), Pos(new_primPlusNat0([])), [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

new_primPlusNat(Zero, []) → Zero

Used ordering: POLO with Polynomial interpretation [25]:

POL(Pos(x₁)) = x₁
POL(Succ(x₁)) = x₁
POL(Zero) = 1
POL([]) = 0
POL(new_primPlusNat(x₁, x₂)) = 2·x₁ + 2·x₂
POL(new_primPlusNat0(x₁)) = 1 + 2·x₁
POL(new_takeWhile(x₁, x₂, x₃)) = x₁ + x₂ + x₃

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(Succ(wv3100)), Pos(Zero), []) → new_takeWhile(Pos(Succ(wv3100)), Pos(new_primPlusNat0([])), [])

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Q is empty.
We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ RuleRemovalProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Pos(wv310), Neg(Succ(Succ(wv30000))), []) → new_takeWhile(Pos(wv310), Neg(Succ(wv30000)), [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

new_takeWhile(Pos(wv310), Neg(Succ(Succ(wv30000))), []) → new_takeWhile(Pos(wv310), Neg(Succ(wv30000)), [])

Strictly oriented rules of the TRS R:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Neg(x₁)) = x₁
POL(Pos(x₁)) = x₁
POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 2
POL([]) = 2
POL(new_primPlusNat(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(new_primPlusNat0(x₁)) = 2·x₁
POL(new_takeWhile(x₁, x₂, x₃)) = x₁ + x₂ + x₃

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ PisEmptyProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000)), []) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000, [])
new_takeWhile11(wv55, wv56, Zero, Zero, []) → new_takeWhile12(wv55, wv56, [])
new_takeWhile12(wv55, Succ(wv560), []) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)), [])
new_takeWhile11(wv55, Succ(wv560), Zero, Succ(wv580), []) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)), [])
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580), []) → new_takeWhile11(wv55, wv56, wv570, wv580, [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Q is empty.
We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_takeWhile12(wv55, Succ(wv560), []) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)), [])
new_takeWhile11(wv55, Succ(wv560), Zero, Succ(wv580), []) → new_takeWhile(Neg(Succ(wv55)), Neg(Succ(wv560)), [])

The remaining pairs can at least be oriented weakly.

new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000)), []) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000, [])
new_takeWhile11(wv55, wv56, Zero, Zero, []) → new_takeWhile12(wv55, wv56, [])
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580), []) → new_takeWhile11(wv55, wv56, wv570, wv580, [])

Used ordering: Polynomial interpretation [25]:

POL(Neg(x₁)) = x₁
POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL([]) = 0
POL(new_primPlusNat(x₁, x₂)) = 1 + x₁
POL(new_primPlusNat0(x₁)) = 1
POL(new_takeWhile(x₁, x₂, x₃)) = x₂
POL(new_takeWhile11(x₁, x₂, x₃, x₄, x₅)) = 1 + x₂
POL(new_takeWhile12(x₁, x₂, x₃)) = 1 + x₂

The following usable rules [17] were oriented:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Succ(wv3100)), Neg(Succ(wv3000)), []) → new_takeWhile11(wv3100, wv3000, wv3100, wv3000, [])
new_takeWhile11(wv55, wv56, Zero, Zero, []) → new_takeWhile12(wv55, wv56, [])
new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580), []) → new_takeWhile11(wv55, wv56, wv570, wv580, [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Q is empty.
We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ RuleRemovalProof

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580), []) → new_takeWhile11(wv55, wv56, wv570, wv580, [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

new_takeWhile11(wv55, wv56, Succ(wv570), Succ(wv580), []) → new_takeWhile11(wv55, wv56, wv570, wv580, [])

Strictly oriented rules of the TRS R:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + 2·x₁
POL(Zero) = 1
POL([]) = 2
POL(new_primPlusNat(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(new_primPlusNat0(x₁)) = 2·x₁
POL(new_takeWhile11(x₁, x₂, x₃, x₄, x₅)) = x₁ + x₂ + x₃ + x₄ + x₅

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ RuleRemovalProof

                                  ↳ QDP

                                    ↳ PisEmptyProof

                      ↳ QDP

                      ↳ QDP

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ RuleRemovalProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Zero), Pos(Zero), []) → new_takeWhile(Neg(Zero), Pos(new_primPlusNat0([])), [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

new_primPlusNat(Zero, []) → Zero

Used ordering: POLO with Polynomial interpretation [25]:

POL(Neg(x₁)) = x₁
POL(Pos(x₁)) = x₁
POL(Succ(x₁)) = x₁
POL(Zero) = 1
POL([]) = 0
POL(new_primPlusNat(x₁, x₂)) = 2·x₁ + 2·x₂
POL(new_primPlusNat0(x₁)) = 1 + 2·x₁
POL(new_takeWhile(x₁, x₂, x₃)) = x₁ + x₂ + x₃

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Zero), Pos(Zero), []) → new_takeWhile(Neg(Zero), Pos(new_primPlusNat0([])), [])

The TRS R consists of the following rules:

new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Q is empty.
We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ RuleRemovalProof

Q DP problem:
The TRS P consists of the following rules:

new_takeWhile(Neg(Zero), Neg(Succ(Succ(wv30000))), []) → new_takeWhile(Neg(Zero), Neg(Succ(wv30000)), [])

The TRS R consists of the following rules:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

new_takeWhile(Neg(Zero), Neg(Succ(Succ(wv30000))), []) → new_takeWhile(Neg(Zero), Neg(Succ(wv30000)), [])

Strictly oriented rules of the TRS R:

new_primPlusNat(Zero, []) → Zero
new_primPlusNat(Succ(wv510), []) → Succ(wv510)
new_primPlusNat0([]) → Succ(Zero)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Neg(x₁)) = x₁
POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 2
POL([]) = 2
POL(new_primPlusNat(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(new_primPlusNat0(x₁)) = 2·x₁
POL(new_takeWhile(x₁, x₂, x₃)) = x₁ + x₂ + x₃

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

takeWhile	p []	= takeWhile3 p []
takeWhile	p (x : xs)	= takeWhile2 p (x : xs)

takeWhile1	p x xs True	= x : takeWhile p xs
takeWhile1	p x xs False	= takeWhile0 p x xs otherwise